Search for: All records

Distributed clause-sharing SAT solvers can solve challenging problems hundreds of times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which limits their use in critical applications. In this work, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. We first describe a simple sequential algorithm and then present a fully distributed algorithm for proof composition, which is substantially more scalable and general than prior works. Our empirical evaluation with over 1500 solver threads shows that our distributed approach allows proof composition and checking within around 3x its own (highly competitive) solving time. 

Test adequacy criteria are widely used to guide test creation. However, many of these criteria are sensitive to statement structure or the choice of test oracle. This is because such criteria ensure that execution reaches the element of interest, but impose no constraints on the execution path after this point. We are not guaranteed to observe a failure just because a fault is triggered. To address this issue, we have proposed the concept of observability—an extension to coverage criteria based on Boolean expressions that combines the obligations of a host criterion with an additional path condition that increases the likelihood that a fault encountered will propagate to a monitored variable. Our study, conducted over five industrial systems and an additional forty open-source systems, has revealed that adding observability tends to improve efficacy over satisfaction of the traditional criteria, with average improvements of 125.98% in mutation detection with the common output-only test oracle and per-model improvements of up to 1760.52%. Ultimately, there is merit to our hypothesis—observability reduces sensitivity to the choice of oracle and to the program structure. 

We report on the effect of the end-Cretaceous impact event on the present-day deep microbial biosphere at the impact site. IODP-ICDP Expedition 364 drilled into the peak ring of the Chicxulub crater, México, allowing us to investigate the microbial communities within this structure. Increased cell biomass was found in the impact suevite, which was deposited within the first few hours of the Cenozoic, demonstrating that the impact produced a new lithological horizon that caused a long-term improvement in deep subsurface colonization potential. In the biologically impoverished granitic rocks, we observed increased cell abundances at impact-induced geological interfaces, that can be attributed to the nutritionally diverse substrates and/or elevated fluid flow. 16S rRNA gene amplicon sequencing revealed taxonomically distinct microbial communities in each crater lithology. These observations show that the impact caused geological deformation that continues to shape the deep subsurface biosphere at Chicxulub in the present day. 

Abstract The Chicxulub crater was formed by an asteroid impact at ca. 66 Ma. The impact is considered to have contributed to the end-Cretaceous mass extinction and reduced productivity in the world’s oceans due to a transient cessation of photosynthesis. Here, biomarker profiles extracted from crater core material reveal exceptional insights into the post-impact upheaval and rapid recovery of microbial life. In the immediate hours to days after the impact, ocean resurge flooded the crater and a subsequent tsunami delivered debris from the surrounding carbonate ramp. Deposited material, including biomarkers diagnostic for land plants, cyanobacteria, and photosynthetic sulfur bacteria, appears to have been mobilized by wave energy from coastal microbial mats. As that energy subsided, days to months later, blooms of unicellular cyanobacteria were fueled by terrigenous nutrients. Approximately 200 k.y. later, the nutrient supply waned and the basin returned to oligotrophic conditions, as evident from N2-fixing cyanobacteria biomarkers. At 1 m.y. after impact, the abundance of photosynthetic sulfur bacteria supported the development of water-column photic zone euxinia within the crater. 

The Cretaceous-Paleogene (K-Pg) mass extinction is marked globally by elevated concentrations of iridium, emplaced by a hypervelocity impact event 66 million years ago. Here, we report new data from four independent laboratories that reveal a positive iridium anomaly within the peak-ring sequence of the Chicxulub impact structure, in drill core recovered by IODP-ICDP Expedition 364. The highest concentration of ultrafine meteoritic matter occurs in the post-impact sediments that cover the crater peak ring, just below the lowermost Danian pelagic limestone. Within years to decades after the impact event, this part of the Chicxulub impact basin returned to a relatively low-energy depositional environment, recording in unprecedented detail the recovery of life during the succeeding millennia. The iridium layer provides a key temporal horizon precisely linking Chicxulub to K-Pg boundary sections worldwide.